Nuprl Lemma : fpf-dom-type
0,22
postcript
pdf
X
,
Y
:Type,
eq
:EqDecider(
Y
),
f
:
x
:
X
fp
Top,
x
:
Y
. strong-subtype(
X
;
Y
)
x
dom(
f
)
x
X
latex
Definitions
A
&
B
,
P
Q
,
P
&
Q
,
S
T
,
P
Q
,
b
,
x
dom(
f
)
,
strong-subtype(
A
;
B
)
,
a
:
A
fp
B
(
a
)
,
x
.
t
(
x
)
,
Top
,
EqDecider(
T
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
deq
wf
,
top
wf
,
fpf
wf
,
strong-subtype
wf
,
fpf-dom
wf
,
assert
wf
,
assert-deq-member
,
strong-subtype-l
member-type
,
subtype-fpf3
origin
X, Y:Type, eq:EqDecider(Y), f:x:X fp
Top, x:Y. strong-subtype(X;Y) 
x 
dom(f) x X X, Y:Type, eq:EqDecider(Y), f:x:X fp Top, x:Y. strong-subtype(X;Y) x dom(f) x X 
Q
T Q
b dom(f) B(a)
x. t(x)x:A. B(x) T